T:Type, L:(T List). (0 < ||L||)  (x:T. (x  L)  ((x = hd(L)))  hd(L) before x  L) 

latex

ProofTree

Definitions	x before y  l, x:AB(x), x:A. B(x), i  j , ||as||, Type, type List, a < b, (x  l), A, hd(l), s = t, P  Q, t  T, x:A  B(x), P & Q, P  Q, P  Q, P  Q, n+m, False, left + right
Lemmas	cons member, cons before, l member wf, not wf, l before wf